$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$, $i$:Id.
\\[0ex]@$i$($x$:$T$) $\Rightarrow$ $\forall$$e$@$i$. $\forall$${\it e'}$$\in$[lastchange($x$;$e$),$e$).($x$ after ${\it e'}$) = ($x$ when $e$) $\in$ $T$